Nuprl Lemma : mul_wf_nzero
11,40
postcript
pdf
a
,
b
:int_nzero. (
a
*
b
)
int_nzero
latex
Definitions
False
,
prop{i:l}
,
P
Q
,
A
,
nequal(
T
;
a
;
b
)
,
t
T
,
int_nzero
,
x
:
A
.
B
(
x
)
,
P
Q
Lemmas
int
nzero
wf
,
nequal
wf
,
int
entire
origin
a,b:int_nzero. (a * b) 
int_nzero a,b:int_nzero. (a * b) int_nzero 
Q
A Tx:A. B(x)
Q